es:event_system{i:l}, e,e':es-E(es). es-le(es; e; e')  (0 < ||[e, e']||) 

latex

Definitions	event_system{i:l}, t  T, x:A. B(x), es-E(es), [e, e'], ||as||, prop{i:l}, es-le(es; e; e'), P  Q, P  Q, P  Q, P  Q, ge(i; j), False, A, A  B, (x  l), x:A. B(x), trans(T; x,y.E(x;y))
Lemmas	es-le-trans, not functionality wrt iff, length zero, member exists, nil member, l member wf, member-es-interval, es-le-self, pos length, es-le wf, length wf1, es-interval wf, es-E wf, event system wf